sort1(nil) -> nil
sort1(cons2(x, y)) -> insert2(x, sort1(y))
insert2(x, nil) -> cons2(x, nil)
insert2(x, cons2(v, w)) -> choose4(x, cons2(v, w), x, v)
choose4(x, cons2(v, w), y, 0) -> cons2(x, cons2(v, w))
choose4(x, cons2(v, w), 0, s1(z)) -> cons2(v, insert2(x, w))
choose4(x, cons2(v, w), s1(y), s1(z)) -> choose4(x, cons2(v, w), y, z)
↳ QTRS
↳ DependencyPairsProof
sort1(nil) -> nil
sort1(cons2(x, y)) -> insert2(x, sort1(y))
insert2(x, nil) -> cons2(x, nil)
insert2(x, cons2(v, w)) -> choose4(x, cons2(v, w), x, v)
choose4(x, cons2(v, w), y, 0) -> cons2(x, cons2(v, w))
choose4(x, cons2(v, w), 0, s1(z)) -> cons2(v, insert2(x, w))
choose4(x, cons2(v, w), s1(y), s1(z)) -> choose4(x, cons2(v, w), y, z)
SORT1(cons2(x, y)) -> INSERT2(x, sort1(y))
INSERT2(x, cons2(v, w)) -> CHOOSE4(x, cons2(v, w), x, v)
CHOOSE4(x, cons2(v, w), s1(y), s1(z)) -> CHOOSE4(x, cons2(v, w), y, z)
CHOOSE4(x, cons2(v, w), 0, s1(z)) -> INSERT2(x, w)
SORT1(cons2(x, y)) -> SORT1(y)
sort1(nil) -> nil
sort1(cons2(x, y)) -> insert2(x, sort1(y))
insert2(x, nil) -> cons2(x, nil)
insert2(x, cons2(v, w)) -> choose4(x, cons2(v, w), x, v)
choose4(x, cons2(v, w), y, 0) -> cons2(x, cons2(v, w))
choose4(x, cons2(v, w), 0, s1(z)) -> cons2(v, insert2(x, w))
choose4(x, cons2(v, w), s1(y), s1(z)) -> choose4(x, cons2(v, w), y, z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
SORT1(cons2(x, y)) -> INSERT2(x, sort1(y))
INSERT2(x, cons2(v, w)) -> CHOOSE4(x, cons2(v, w), x, v)
CHOOSE4(x, cons2(v, w), s1(y), s1(z)) -> CHOOSE4(x, cons2(v, w), y, z)
CHOOSE4(x, cons2(v, w), 0, s1(z)) -> INSERT2(x, w)
SORT1(cons2(x, y)) -> SORT1(y)
sort1(nil) -> nil
sort1(cons2(x, y)) -> insert2(x, sort1(y))
insert2(x, nil) -> cons2(x, nil)
insert2(x, cons2(v, w)) -> choose4(x, cons2(v, w), x, v)
choose4(x, cons2(v, w), y, 0) -> cons2(x, cons2(v, w))
choose4(x, cons2(v, w), 0, s1(z)) -> cons2(v, insert2(x, w))
choose4(x, cons2(v, w), s1(y), s1(z)) -> choose4(x, cons2(v, w), y, z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
INSERT2(x, cons2(v, w)) -> CHOOSE4(x, cons2(v, w), x, v)
CHOOSE4(x, cons2(v, w), s1(y), s1(z)) -> CHOOSE4(x, cons2(v, w), y, z)
CHOOSE4(x, cons2(v, w), 0, s1(z)) -> INSERT2(x, w)
sort1(nil) -> nil
sort1(cons2(x, y)) -> insert2(x, sort1(y))
insert2(x, nil) -> cons2(x, nil)
insert2(x, cons2(v, w)) -> choose4(x, cons2(v, w), x, v)
choose4(x, cons2(v, w), y, 0) -> cons2(x, cons2(v, w))
choose4(x, cons2(v, w), 0, s1(z)) -> cons2(v, insert2(x, w))
choose4(x, cons2(v, w), s1(y), s1(z)) -> choose4(x, cons2(v, w), y, z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
INSERT2(x, cons2(v, w)) -> CHOOSE4(x, cons2(v, w), x, v)
CHOOSE4(x, cons2(v, w), s1(y), s1(z)) -> CHOOSE4(x, cons2(v, w), y, z)
CHOOSE4(x, cons2(v, w), 0, s1(z)) -> INSERT2(x, w)
POL(0) = 0
POL(CHOOSE4(x1, x2, x3, x4)) = 1 + x2 + x4
POL(INSERT2(x1, x2)) = 2·x2
POL(cons2(x1, x2)) = 2 + x1 + 2·x2
POL(s1(x1)) = 2 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
sort1(nil) -> nil
sort1(cons2(x, y)) -> insert2(x, sort1(y))
insert2(x, nil) -> cons2(x, nil)
insert2(x, cons2(v, w)) -> choose4(x, cons2(v, w), x, v)
choose4(x, cons2(v, w), y, 0) -> cons2(x, cons2(v, w))
choose4(x, cons2(v, w), 0, s1(z)) -> cons2(v, insert2(x, w))
choose4(x, cons2(v, w), s1(y), s1(z)) -> choose4(x, cons2(v, w), y, z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
SORT1(cons2(x, y)) -> SORT1(y)
sort1(nil) -> nil
sort1(cons2(x, y)) -> insert2(x, sort1(y))
insert2(x, nil) -> cons2(x, nil)
insert2(x, cons2(v, w)) -> choose4(x, cons2(v, w), x, v)
choose4(x, cons2(v, w), y, 0) -> cons2(x, cons2(v, w))
choose4(x, cons2(v, w), 0, s1(z)) -> cons2(v, insert2(x, w))
choose4(x, cons2(v, w), s1(y), s1(z)) -> choose4(x, cons2(v, w), y, z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SORT1(cons2(x, y)) -> SORT1(y)
POL(SORT1(x1)) = 2·x1
POL(cons2(x1, x2)) = 1 + 2·x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
sort1(nil) -> nil
sort1(cons2(x, y)) -> insert2(x, sort1(y))
insert2(x, nil) -> cons2(x, nil)
insert2(x, cons2(v, w)) -> choose4(x, cons2(v, w), x, v)
choose4(x, cons2(v, w), y, 0) -> cons2(x, cons2(v, w))
choose4(x, cons2(v, w), 0, s1(z)) -> cons2(v, insert2(x, w))
choose4(x, cons2(v, w), s1(y), s1(z)) -> choose4(x, cons2(v, w), y, z)